FDL - Nuprl Lemma : es-when-first

Nuprl Lemma : es-when-first

11,40

es:event_system{i:l}, e:es-E(es), x:Id.
(

es-first(es; e))

sqequal(es-when(es; x; e); (es_init(es)(loc(e),x,0 + es-time(es; e))))

Definitions b, t T, P Q, x:A. B(x), es-when(es; x; e), event_system{i:l}, es-E(es), Id, es-first(es; e)

Lemmas assert wf, es-first wf, Id wf, es-E wf, event system wf, state-when-first

Definitions	b, t T, P Q, x:A. B(x), es-when(es; x; e), event_system{i:l}, es-E(es), Id, es-first(es; e)
Lemmas	assert wf, es-first wf, Id wf, es-E wf, event system wf, state-when-first